hasproperty(ctxm(dot,al,d_2,id_2,cd_2),ctxm(dot,al,d_4,id_4,cd_4),gt60).
hasproperty(ctxm(kappa_,al,d_2,id_2,cd_2),ctxm(kappa_,al,d_4,id_4,cd_4),gt60).
hasproperty(ctxm(zeta_,u,d_2,id_2,cd_2),ctxm(zeta_,u,d_4,id_4,cd_4),gt60).
hasproperty(ctxm(xi_,u,d_2,id_2,cd_2),ctxm(xi_,u,d_4,id_4,cd_4),gt60).

knows(ttp,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(ttp,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(ttp,ctxm(dot,is,ip,ip_is,ip_is)).
knows(ttp,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(ttp,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(ttp,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(ttp,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(ttp,ctxm(dot,ttp,kM,kM_ttp,kM_ttp)).
knows(ttp,ctxm(dot,ls,ip,ip_ls,ip_ls)).
knows(ttp,pri(pk,[ctxm(dot,ls,kM,kM_ls,kM_ls)])).
knows(ttp,ctxm(dot,ls,i,i_ls,i_ls)).
knows(ttp,ctxm(dot,is,i,i_is,i_is)).
knows(ii,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(ii,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(ii,ctxm(dot,is,ip,ip_is,ip_is)).
knows(ii,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(ii,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(ii,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(ii,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(ii,ctxm(dot,ii,kM,kM_ii,kM_ii)).
knows(ii,ctxm(kappa_,al,i_ii,i_al_ii,i_al_ii)).
knows(ii,ctxm(kappa_,al,d_1,id_1,cd_1)).
knows(ii,ctxm(kappa_,al,d_2,id_2,cd_2)).
knows(ii,ctxm(kappa_,al,d_3,id_3,cd_3)).
knows(ii,ctxm(pi_,u,i_ii,i_al_ii,i_al_ii)).

knows(ii,ctxm(dot,ls,ip,ip_ls,ip_ls)).
knows(ii,pri(pk,[ctxm(dot,ls,kM,kM_ls,kM_ls)])).
knows(ii,ctxm(dot,ls,i,i_ls,i_ls)).
knows(ii,ctxm(dot,is,i,i_is,i_is)).
knows(ii,ctxm(pi_,u,i_idp1_ls,il1,il1)).
knows(ii,ctxm(pi_,dot,n,ss(pi_,in),ss(pi_,cn))).
knows(ii,ctxm(zeta_,u,i_ii,i_al_ii,i_al_ii)).
knows(ii,ctxm(zeta_,u,i_sess,ss(zeta_,i_sess),ss(zeta_,i_sess))).
knows(ii,ctxm(zeta_,dot,n,ss(zeta_,n1),ss(zeta_,cn1))).
knows(ii,ctxm(xi_,u,i_ii,i_al_ii,i_al_ii)).
knows(ii,ctxm(xi_,u,i_sess,ss(xi_,i_sess),ss(xi_,i_sess))).
knows(ii,ctxm(xi_,dot,n,ss(xi_,n1),ss(xi_,cn1))).

knows(is,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(is,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(is,ctxm(dot,is,ip,ip_is,ip_is)).
knows(is,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(is,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(is,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(is,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(is,ctxm(dot,is,kM,kM_is,kM_is)).
knows(is,ctxm(mu_,al,i_is,i_al_is,i_al_is)).
knows(is,ctxm(mu_,al,d_5,id_5,cd_5)).
knows(is,ctxm(mu_,al,d_6,id_6,cd_6)).
knows(is,ctxm(eta_,u,i_is,i_al_is,i_al_is)).

knows(is,ctxm(dot,ls,ip,ip_ls,ip_ls)).
knows(is,pri(pk,[ctxm(dot,ls,kM,kM_ls,kM_ls)])).
knows(is,ctxm(dot,ls,i,i_ls,i_ls)).
knows(is,ctxm(dot,is,i,i_is,i_is)).
knows(is,ctxm(eta_,u,i_idp2_ls,il2,il2)).
knows(is,ctxm(eta_,dot,n,ss(eta_,in),ss(eta_,cn))).

knows(bs,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(bs,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(bs,ctxm(dot,is,ip,ip_is,ip_is)).
knows(bs,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(bs,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(bs,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(bs,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(bs,ctxm(dot,bs,kM,kM_bs,kM_bs)).
knows(bs,ctxm(zeta_,u,d_7,id_71,cd_71)).
knows(bs,ctxm(xi_,u,d_7,id_72,cd_72)).

knows(bs,ctxm(dot,ls,ip,ip_ls,ip_ls)).
knows(bs,pri(pk,[ctxm(dot,ls,kM,kM_ls,kM_ls)])).
knows(bs,ctxm(dot,ls,i,i_ls,i_ls)).
knows(bs,ctxm(dot,is,i,i_is,i_is)).

knows(al,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(al,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(al,ctxm(dot,is,ip,ip_is,ip_is)).
knows(al,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(al,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(al,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(al,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).
knows(al,ctxm(dot,al,i,i_al,i_al)).
knows(al,ctxm(dot,al,i_ii,i_al_ii,i_al_ii)).
knows(al,ctxm(dot,al,i_is,i_al_is,i_al_is)).
knows(al,ctxm(dot,al,d_1,id_1,cd_1)).
knows(al,ctxm(dot,al,d_2,id_2,cd_2)).
knows(al,ctxm(dot,al,d_3,id_3,cd_3)).
knows(al,ctxm(dot,al,d_5,id_5,cd_5)).
knows(al,ctxm(dot,al,d_6,id_6,cd_6)).
knows(al,ctxm(pi_,u,i_ii,i_al_ii,i_al_ii)).
knows(al,ctxm(eta_,u,i_is,i_al_is,i_al_is)).
knows(al,ctxm(zeta_,u,i,i_al,i_al)).
knows(al,ctxm(xi_,u,i,i_al,i_al)).
knows(al,ctxm(pi_,u,ip,ip_al_1,ip_al_1)).
knows(al,ctxm(eta_,u,ip,ip_al_2,ip_al_2)).
knows(al,ctxm(zeta_,u,ip,ip_al_3,ip_al_3)).
knows(al,ctxm(xi_,u,ip,ip_al_4,ip_al_4)).
knows(al,ctxm(dot,ls,ip,ip_ls,ip_ls)).
knows(al,pri(pk,[ctxm(dot,ls,kM,kM_ls,kM_ls)])).
knows(al,ctxm(dot,ls,i,i_ls,i_ls)).
knows(al,ctxm(dot,is,i,i_is,i_is)).

knows(ls,ctxm(dot,ii,ip,ip_ii,ip_ii)).
knows(ls,pri(pk,[ctxm(dot,ii,kM,kM_ii,kM_ii)])).
knows(ls,ctxm(dot,is,ip,ip_is,ip_is)).
knows(ls,pri(pk,[ctxm(dot,is,kM,kM_is,kM_is)])).
knows(ls,ctxm(dot,bs,ip,ip_bs,ip_bs)).
knows(ls,pri(pk,[ctxm(dot,bs,kM,kM_bs,kM_bs)])).
knows(ls,pri(pk,[ctxm(dot,ttp,kM,kM_ttp,kM_ttp)])).

knows(ls,ctxm(dot,ls,ip,ip_ls,ip_ls)).
knows(ls,pri(pk,[ctxm(dot,ls,kM,kM_ls,kM_ls)])).
knows(ls,ctxm(dot,ls,kM,kM_ls,kM_ls)).
knows(ls,ctxm(dot,ls,i,i_ls,i_ls)).
knows(ls,ctxm(dot,is,i,i_is,i_is)).
knows(ls,ctxm(nu_,al,i_l,i_al_l,i_al_l)).
knows(ls,ctxm(pi_,u,i_l,i_al_l,i_al_l)).
knows(ls,ctxm(eta_,u,i_l,i_al_l,i_al_l)).
knows(ls,ctxm(zeta_,dot,nI,ss(zeta_,nn),ss(zeta_,cn2))).
knows(ls,ctxm(xi_,dot,nI,ss(xi_,nn),ss(xi_,cn2))).
